T:Type, L1, L2:T List. L1  L2  L2  L1  L1 = L2 

latex

Definitions	||as||, P  Q, x:A. B(x), t  T, L1  L2
Lemmas	length sublist, length wf1, sublist wf, proper sublist length